module MeteoCal

open util/boolean

//////////////////////////////
//////SUGNATURES///////
/////////////////////////////

sig ExternalUser, Weather,Username, Password, Message, Float {}
//These signatures are considered empty  for semplicity because their attributes are not useful for the Alloy modelization.
//String attributes are not considered for semplicity because they are not useful for the Alloy modelization.

sig Date{
		timestamp: one Int //unix timestamp (a day is represented by its first second)
	}{
	timestamp >=0
	}
	
sig Day {
		dailyPublicEvents: set Event,
		date: one Date,
		Weather: one Weather
		}

sig Event {
		day: one Day,
		privacy: one Bool,
		organizer: one User,
		partecipants: some User
	}{
	//Organizer must be a partecipant.
		organizer in partecipants
	 
	//No 2 partecipants with same username.
		all p1,p2: partecipants | p1.username=p2.username implies p1=p2

	//If private, partecipants collapse in the organizer.
		privacy = True implies #partecipants=1
	}


sig Calendar {
		owner: one User,
		privacy:one Bool,
		busyDays: set Day,
		freeDays: set Day
	}{
	//Disjuntion between busyDays and freeDays.
		no (busyDays & freeDays)
	//No duplications
		all d1,d2: busyDays | d1.date=d2.date implies d1=d2
		all d1,d2: freeDays | d1.date=d2.date implies d1=d2
		all d:Day | d in busyDays || d in freeDays
	}

sig User {
		username: one Username,
		password: one Password,
		otherEvents: set Event,
		ownEvents: set Event,
		calendar: one Calendar,
		notifications: set Notification,
		friends: set User,
		reliability: one Reliability
	}{
	//Disjuntion between ownEvents and otherEvents.
		no (ownEvents & otherEvents)

	//No conflicting events
	all disj e1,e2: userEvents |e1.day!=e2.day

	}

sig Notification {
		sender: one User,
		receiver: one User,
		mex: one Message,
		day: one Date
	}{
	//Sender not = receiver.
		sender != receiver
	}

sig WeatherNotification extends Notification {}

sig FriendNotification extends Notification {}

sig EventNotification extends Notification {}

sig Reliability{
		owner: one User,
		average: one Float,
	}

		


/////////////////////////
/////FUNCTIONS/////
////////////////////////

//Returns the entire set of events of a given user.
fun userEvents [u: User] :some Event{
		u.(ownEvents + otherEvents)
}

////////////////////////
//////FACTS//////////
///////////////////////

//Simmetries
	fact simmetries{
					all e:Event | e in e.organizer.ownEvents
					all u:User | all e:u.ownEvents | u=e.organizer
					all e:Event | all p:e.partecipants | p!=e.organizer implies e in p.otherEvents
					all u:User | all e:u.otherEvents | u in e.partecipants
					all d:Day | all e: d.dailyPublicEvents | e.day=d
					all e:Event | e in e.day.dailyPublicEvents
					all u:User | u.reliability.owner = u
					all r:Reliability | r.owner.reliability = r
					all c:Calendar | c.owner.calendar = c
					all u:User | u.calendar.owner = u
					all u:User | u !in u.friends
					all u:User | all f: u.friends | u in f.friends
					all n:Notification | n in n.receiver.notifications && n in n.sender.notifications
					all u:User | all n: u.notifications | n.receiver = u || n.sender = u
					all n:Notification | n in WeatherNotification || n in EventNotification || n in FriendNotification
					all wn:WeatherNotification,en:EventNotification,fn:FriendNotification | wn.mex != en.mex && wn.mex!= fn.mex && en.mex != fn.mex
				}
//Privacy
	fact privacy{
					all d:Day | all e: d.dailyPublicEvents | e.privacy = False
				}

//No duplications

	fact noDuplications {
					all u1,u2:User | u1.username = u2.username implies u1=u2
					all e1,e2:Event | (e1.day = e2.day) implies e1=e2
					all d1,d2:Date | d1.timestamp = d2.timestamp implies d1=d2
					all c1,c2:Calendar | c1.owner = c2.owner implies c1=c2
					all d1,d2: Day | d1.date = d2.date implies d1=d2
				}


/////////////////////////////
/////ASSERTIONS////////
////////////////////////////

//Many of these assertions have the same code of facts. This is because in a first moment there weren't no facts, 
//then thanks of assertions we found right constraints to apply in order to make the system consistent.

assert notificationSimmetry{
					all n:Notification | n in n.receiver.notifications && n in n.sender.notifications
					all u:User | all n: u.notifications | n.receiver = u || n.sender = u
					all n:Notification | n in WeatherNotification || n in EventNotification || n in FriendNotification
					all wn:WeatherNotification,en:EventNotification,fn:FriendNotification | wn.mex != en.mex && wn.mex!= fn.mex && en.mex != fn.mex
					}
check notificationSimmetry

assert dayEventSimmetry{
					all d:Day | all e: d.dailyPublicEvents | e.day=d
					all e:Event | e in e.day.dailyPublicEvents
					}
check dayEventSimmetry

assert userEventSimmetry{
					all e:Event | e in e.organizer.ownEvents
					all u:User | all e:u.ownEvents | u=e.organizer
					all e:Event | all p:e.partecipants | p!=e.organizer implies e in p.otherEvents
					all u:User | all e:u.otherEvents | u in e.partecipants
					}
check userEventSimmetry

assert noDuplications{
			all u1,u2:User | u1.username = u2.username implies u1=u2
			all e1,e2:Event | (e1.day = e2.day) implies e1=e2
			all d1,d2:Date | d1.timestamp = d2.timestamp implies d1=d2
			all c1,c2:Calendar | c1.owner = c2.owner implies c1=c2
			all d1,d2: Day | d1.date = d2.date implies d1=d2
			}
check noDuplications

assert coherence {
		#User = #Calendar 
		#User = #Reliability
		}
check coherence 

assert privacy {
		(all e:Event | e.privacy = True) implies (all d:Day | #d.dailyPublicEvents = 0)
		
		}
check privacy




pred show(){
		#User = 2
		#Event = 2
	}
run show



/////////////////////////////
//SYSTEM FUNCTIONS//
/////////////////////////////

//To better understand how this system works, predicate/functions listed below show main procedures that can be applied on/by the system.


sig DataBase{
		users: set User,
		calendars: set Calendar,
		events: set Event,
		notifications: set Notification
		}{
		#DataBase = 1
		all u: User | u in users
		all c: Calendar | c in calendars
		all e: Event | e in events
		all n:Notification | n in notifications
		}

// Database predicates examples
pred addUser [d: DataBase, u:User]{
		u !in d.users implies d.users = d.users + u
		}
run addUser

pred addEvent[d: DataBase, e:Event]{
		e !in d.events implies d.events = d.events + e
		}
run addEvent

pred deleteEvent [d: DataBase, e:Event]{
		e in d.events && (no d:Day | e in d.dailyPublicEvents) && (no u:User | (e in u.ownEvents || e in u.otherEvents)) implies d.events = d.events - e
		}
run deleteEvent

pred logIn [eu:ExternalUser, un:Username, p:Password]{
		one u:User | u.username = un && u.password = p
		}
run logIn

















